H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.785 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((sinh :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((sinh :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((sinh :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(sinh :: Float -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sinh",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sinh vx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="(exp vx3 - exp (`negate` vx3)) / fromInt (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="primDivFloat (exp vx3 - exp (`negate` vx3)) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6 -> 16[label="",style="dashed", color="red", weight=0];
6[label="primDivFloat (primMinusFloat (exp vx3) (exp (`negate` vx3))) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="magenta"];6 -> 17[label="",style="dashed", color="magenta", weight=3];
6 -> 18[label="",style="dashed", color="magenta", weight=3];
17[label="exp (`negate` vx3)",fontsize=16,color="black",shape="box"];17 -> 20[label="",style="solid", color="black", weight=3];
18[label="exp vx3",fontsize=16,color="black",shape="box"];18 -> 21[label="",style="solid", color="black", weight=3];
16[label="primDivFloat (primMinusFloat vx4 vx5) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="burlywood",shape="triangle"];187[label="vx4/Float vx40 vx41",fontsize=10,color="white",style="solid",shape="box"];16 -> 187[label="",style="solid", color="burlywood", weight=9];
187 -> 22[label="",style="solid", color="burlywood", weight=3];
20[label="primExpFloat (`negate` vx3)",fontsize=16,color="black",shape="box"];20 -> 23[label="",style="solid", color="black", weight=3];
21[label="primExpFloat vx3",fontsize=16,color="black",shape="box"];21 -> 24[label="",style="solid", color="black", weight=3];
22[label="primDivFloat (primMinusFloat (Float vx40 vx41) vx5) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="burlywood",shape="box"];188[label="vx5/Float vx50 vx51",fontsize=10,color="white",style="solid",shape="box"];22 -> 188[label="",style="solid", color="burlywood", weight=9];
188 -> 25[label="",style="solid", color="burlywood", weight=3];
23[label="terminator (`negate` vx3)",fontsize=16,color="black",shape="box"];23 -> 26[label="",style="solid", color="black", weight=3];
24[label="terminator vx3",fontsize=16,color="black",shape="box"];24 -> 27[label="",style="solid", color="black", weight=3];
25[label="primDivFloat (primMinusFloat (Float vx40 vx41) (Float vx50 vx51)) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];25 -> 28[label="",style="solid", color="black", weight=3];
26[label="ter1m (`negate` vx3)",fontsize=16,color="green",shape="box"];26 -> 29[label="",style="dashed", color="green", weight=3];
27[label="ter2m vx3",fontsize=16,color="green",shape="box"];27 -> 30[label="",style="dashed", color="green", weight=3];
28[label="primDivFloat (Float (vx40 - vx50) (vx41 * vx51)) (fromInt (Pos (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];28 -> 31[label="",style="solid", color="black", weight=3];
29[label="`negate` vx3",fontsize=16,color="black",shape="box"];29 -> 32[label="",style="solid", color="black", weight=3];
30[label="vx3",fontsize=16,color="green",shape="box"];31[label="primDivFloat (Float (vx40 - vx50) (vx41 * vx51)) (primIntToFloat (Pos (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];31 -> 33[label="",style="solid", color="black", weight=3];
32[label="primNegFloat vx3",fontsize=16,color="burlywood",shape="box"];189[label="vx3/Float vx30 vx31",fontsize=10,color="white",style="solid",shape="box"];32 -> 189[label="",style="solid", color="burlywood", weight=9];
189 -> 34[label="",style="solid", color="burlywood", weight=3];
33[label="primDivFloat (Float (vx40 - vx50) (vx41 * vx51)) (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];33 -> 35[label="",style="solid", color="black", weight=3];
34[label="primNegFloat (Float vx30 vx31)",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="Float ((vx40 - vx50) * Pos (Succ Zero)) (vx41 * vx51 * Pos (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];35 -> 37[label="",style="dashed", color="green", weight=3];
35 -> 38[label="",style="dashed", color="green", weight=3];
36[label="Float (`negate` vx30) vx31",fontsize=16,color="green",shape="box"];36 -> 39[label="",style="dashed", color="green", weight=3];
37[label="(vx40 - vx50) * Pos (Succ Zero)",fontsize=16,color="black",shape="box"];37 -> 40[label="",style="solid", color="black", weight=3];
38[label="vx41 * vx51 * Pos (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];38 -> 41[label="",style="solid", color="black", weight=3];
39[label="`negate` vx30",fontsize=16,color="black",shape="box"];39 -> 42[label="",style="solid", color="black", weight=3];
40[label="primMulInt (vx40 - vx50) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];40 -> 43[label="",style="solid", color="black", weight=3];
41[label="primMulInt (vx41 * vx51) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];41 -> 44[label="",style="solid", color="black", weight=3];
42[label="primNegInt vx30",fontsize=16,color="burlywood",shape="box"];190[label="vx30/Pos vx300",fontsize=10,color="white",style="solid",shape="box"];42 -> 190[label="",style="solid", color="burlywood", weight=9];
190 -> 45[label="",style="solid", color="burlywood", weight=3];
191[label="vx30/Neg vx300",fontsize=10,color="white",style="solid",shape="box"];42 -> 191[label="",style="solid", color="burlywood", weight=9];
191 -> 46[label="",style="solid", color="burlywood", weight=3];
43[label="primMulInt (primMinusInt vx40 vx50) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];192[label="vx40/Pos vx400",fontsize=10,color="white",style="solid",shape="box"];43 -> 192[label="",style="solid", color="burlywood", weight=9];
192 -> 47[label="",style="solid", color="burlywood", weight=3];
193[label="vx40/Neg vx400",fontsize=10,color="white",style="solid",shape="box"];43 -> 193[label="",style="solid", color="burlywood", weight=9];
193 -> 48[label="",style="solid", color="burlywood", weight=3];
44[label="primMulInt (primMulInt vx41 vx51) (Pos (Succ (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];194[label="vx41/Pos vx410",fontsize=10,color="white",style="solid",shape="box"];44 -> 194[label="",style="solid", color="burlywood", weight=9];
194 -> 49[label="",style="solid", color="burlywood", weight=3];
195[label="vx41/Neg vx410",fontsize=10,color="white",style="solid",shape="box"];44 -> 195[label="",style="solid", color="burlywood", weight=9];
195 -> 50[label="",style="solid", color="burlywood", weight=3];
45[label="primNegInt (Pos vx300)",fontsize=16,color="black",shape="box"];45 -> 51[label="",style="solid", color="black", weight=3];
46[label="primNegInt (Neg vx300)",fontsize=16,color="black",shape="box"];46 -> 52[label="",style="solid", color="black", weight=3];
47[label="primMulInt (primMinusInt (Pos vx400) vx50) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];196[label="vx50/Pos vx500",fontsize=10,color="white",style="solid",shape="box"];47 -> 196[label="",style="solid", color="burlywood", weight=9];
196 -> 53[label="",style="solid", color="burlywood", weight=3];
197[label="vx50/Neg vx500",fontsize=10,color="white",style="solid",shape="box"];47 -> 197[label="",style="solid", color="burlywood", weight=9];
197 -> 54[label="",style="solid", color="burlywood", weight=3];
48[label="primMulInt (primMinusInt (Neg vx400) vx50) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];198[label="vx50/Pos vx500",fontsize=10,color="white",style="solid",shape="box"];48 -> 198[label="",style="solid", color="burlywood", weight=9];
198 -> 55[label="",style="solid", color="burlywood", weight=3];
199[label="vx50/Neg vx500",fontsize=10,color="white",style="solid",shape="box"];48 -> 199[label="",style="solid", color="burlywood", weight=9];
199 -> 56[label="",style="solid", color="burlywood", weight=3];
49[label="primMulInt (primMulInt (Pos vx410) vx51) (Pos (Succ (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];200[label="vx51/Pos vx510",fontsize=10,color="white",style="solid",shape="box"];49 -> 200[label="",style="solid", color="burlywood", weight=9];
200 -> 57[label="",style="solid", color="burlywood", weight=3];
201[label="vx51/Neg vx510",fontsize=10,color="white",style="solid",shape="box"];49 -> 201[label="",style="solid", color="burlywood", weight=9];
201 -> 58[label="",style="solid", color="burlywood", weight=3];
50[label="primMulInt (primMulInt (Neg vx410) vx51) (Pos (Succ (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];202[label="vx51/Pos vx510",fontsize=10,color="white",style="solid",shape="box"];50 -> 202[label="",style="solid", color="burlywood", weight=9];
202 -> 59[label="",style="solid", color="burlywood", weight=3];
203[label="vx51/Neg vx510",fontsize=10,color="white",style="solid",shape="box"];50 -> 203[label="",style="solid", color="burlywood", weight=9];
203 -> 60[label="",style="solid", color="burlywood", weight=3];
51[label="Neg vx300",fontsize=16,color="green",shape="box"];52[label="Pos vx300",fontsize=16,color="green",shape="box"];53[label="primMulInt (primMinusInt (Pos vx400) (Pos vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];53 -> 61[label="",style="solid", color="black", weight=3];
54[label="primMulInt (primMinusInt (Pos vx400) (Neg vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];54 -> 62[label="",style="solid", color="black", weight=3];
55[label="primMulInt (primMinusInt (Neg vx400) (Pos vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];55 -> 63[label="",style="solid", color="black", weight=3];
56[label="primMulInt (primMinusInt (Neg vx400) (Neg vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];56 -> 64[label="",style="solid", color="black", weight=3];
57[label="primMulInt (primMulInt (Pos vx410) (Pos vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];57 -> 65[label="",style="solid", color="black", weight=3];
58[label="primMulInt (primMulInt (Pos vx410) (Neg vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59[label="primMulInt (primMulInt (Neg vx410) (Pos vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];59 -> 67[label="",style="solid", color="black", weight=3];
60[label="primMulInt (primMulInt (Neg vx410) (Neg vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="primMulInt (primMinusNat vx400 vx500) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="triangle"];204[label="vx400/Succ vx4000",fontsize=10,color="white",style="solid",shape="box"];61 -> 204[label="",style="solid", color="burlywood", weight=9];
204 -> 69[label="",style="solid", color="burlywood", weight=3];
205[label="vx400/Zero",fontsize=10,color="white",style="solid",shape="box"];61 -> 205[label="",style="solid", color="burlywood", weight=9];
205 -> 70[label="",style="solid", color="burlywood", weight=3];
62[label="primMulInt (Pos (primPlusNat vx400 vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];62 -> 71[label="",style="solid", color="black", weight=3];
63[label="primMulInt (Neg (primPlusNat vx400 vx500)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];63 -> 72[label="",style="solid", color="black", weight=3];
64 -> 61[label="",style="dashed", color="red", weight=0];
64[label="primMulInt (primMinusNat vx500 vx400) (Pos (Succ Zero))",fontsize=16,color="magenta"];64 -> 73[label="",style="dashed", color="magenta", weight=3];
64 -> 74[label="",style="dashed", color="magenta", weight=3];
65[label="primMulInt (Pos (primMulNat vx410 vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="triangle"];65 -> 75[label="",style="solid", color="black", weight=3];
66[label="primMulInt (Neg (primMulNat vx410 vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="triangle"];66 -> 76[label="",style="solid", color="black", weight=3];
67 -> 66[label="",style="dashed", color="red", weight=0];
67[label="primMulInt (Neg (primMulNat vx410 vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="magenta"];67 -> 77[label="",style="dashed", color="magenta", weight=3];
67 -> 78[label="",style="dashed", color="magenta", weight=3];
68 -> 65[label="",style="dashed", color="red", weight=0];
68[label="primMulInt (Pos (primMulNat vx410 vx510)) (Pos (Succ (Succ Zero)))",fontsize=16,color="magenta"];68 -> 79[label="",style="dashed", color="magenta", weight=3];
68 -> 80[label="",style="dashed", color="magenta", weight=3];
69[label="primMulInt (primMinusNat (Succ vx4000) vx500) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];209[label="vx500/Succ vx5000",fontsize=10,color="white",style="solid",shape="box"];69 -> 209[label="",style="solid", color="burlywood", weight=9];
209 -> 81[label="",style="solid", color="burlywood", weight=3];
210[label="vx500/Zero",fontsize=10,color="white",style="solid",shape="box"];69 -> 210[label="",style="solid", color="burlywood", weight=9];
210 -> 82[label="",style="solid", color="burlywood", weight=3];
70[label="primMulInt (primMinusNat Zero vx500) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];211[label="vx500/Succ vx5000",fontsize=10,color="white",style="solid",shape="box"];70 -> 211[label="",style="solid", color="burlywood", weight=9];
211 -> 83[label="",style="solid", color="burlywood", weight=3];
212[label="vx500/Zero",fontsize=10,color="white",style="solid",shape="box"];70 -> 212[label="",style="solid", color="burlywood", weight=9];
212 -> 84[label="",style="solid", color="burlywood", weight=3];
71[label="Pos (primMulNat (primPlusNat vx400 vx500) (Succ Zero))",fontsize=16,color="green",shape="box"];71 -> 85[label="",style="dashed", color="green", weight=3];
72[label="Neg (primMulNat (primPlusNat vx400 vx500) (Succ Zero))",fontsize=16,color="green",shape="box"];72 -> 86[label="",style="dashed", color="green", weight=3];
73[label="vx400",fontsize=16,color="green",shape="box"];74[label="vx500",fontsize=16,color="green",shape="box"];75[label="Pos (primMulNat (primMulNat vx410 vx510) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];75 -> 87[label="",style="dashed", color="green", weight=3];
76[label="Neg (primMulNat (primMulNat vx410 vx510) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];76 -> 88[label="",style="dashed", color="green", weight=3];
77[label="vx410",fontsize=16,color="green",shape="box"];78[label="vx510",fontsize=16,color="green",shape="box"];79[label="vx510",fontsize=16,color="green",shape="box"];80[label="vx410",fontsize=16,color="green",shape="box"];81[label="primMulInt (primMinusNat (Succ vx4000) (Succ vx5000)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];81 -> 89[label="",style="solid", color="black", weight=3];
82[label="primMulInt (primMinusNat (Succ vx4000) Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];82 -> 90[label="",style="solid", color="black", weight=3];
83[label="primMulInt (primMinusNat Zero (Succ vx5000)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];83 -> 91[label="",style="solid", color="black", weight=3];
84[label="primMulInt (primMinusNat Zero Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];84 -> 92[label="",style="solid", color="black", weight=3];
85[label="primMulNat (primPlusNat vx400 vx500) (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];213[label="vx400/Succ vx4000",fontsize=10,color="white",style="solid",shape="box"];85 -> 213[label="",style="solid", color="burlywood", weight=9];
213 -> 93[label="",style="solid", color="burlywood", weight=3];
214[label="vx400/Zero",fontsize=10,color="white",style="solid",shape="box"];85 -> 214[label="",style="solid", color="burlywood", weight=9];
214 -> 94[label="",style="solid", color="burlywood", weight=3];
86 -> 85[label="",style="dashed", color="red", weight=0];
86[label="primMulNat (primPlusNat vx400 vx500) (Succ Zero)",fontsize=16,color="magenta"];86 -> 95[label="",style="dashed", color="magenta", weight=3];
86 -> 96[label="",style="dashed", color="magenta", weight=3];
87 -> 141[label="",style="dashed", color="red", weight=0];
87[label="primMulNat (primMulNat vx410 vx510) (Succ (Succ Zero))",fontsize=16,color="magenta"];87 -> 142[label="",style="dashed", color="magenta", weight=3];
88 -> 141[label="",style="dashed", color="red", weight=0];
88[label="primMulNat (primMulNat vx410 vx510) (Succ (Succ Zero))",fontsize=16,color="magenta"];88 -> 143[label="",style="dashed", color="magenta", weight=3];
89 -> 61[label="",style="dashed", color="red", weight=0];
89[label="primMulInt (primMinusNat vx4000 vx5000) (Pos (Succ Zero))",fontsize=16,color="magenta"];89 -> 100[label="",style="dashed", color="magenta", weight=3];
89 -> 101[label="",style="dashed", color="magenta", weight=3];
90[label="primMulInt (Pos (Succ vx4000)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];90 -> 102[label="",style="solid", color="black", weight=3];
91[label="primMulInt (Neg (Succ vx5000)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];91 -> 103[label="",style="solid", color="black", weight=3];
92[label="primMulInt (Pos Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];92 -> 104[label="",style="solid", color="black", weight=3];
93[label="primMulNat (primPlusNat (Succ vx4000) vx500) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];219[label="vx500/Succ vx5000",fontsize=10,color="white",style="solid",shape="box"];93 -> 219[label="",style="solid", color="burlywood", weight=9];
219 -> 105[label="",style="solid", color="burlywood", weight=3];
220[label="vx500/Zero",fontsize=10,color="white",style="solid",shape="box"];93 -> 220[label="",style="solid", color="burlywood", weight=9];
220 -> 106[label="",style="solid", color="burlywood", weight=3];
94[label="primMulNat (primPlusNat Zero vx500) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];221[label="vx500/Succ vx5000",fontsize=10,color="white",style="solid",shape="box"];94 -> 221[label="",style="solid", color="burlywood", weight=9];
221 -> 107[label="",style="solid", color="burlywood", weight=3];
222[label="vx500/Zero",fontsize=10,color="white",style="solid",shape="box"];94 -> 222[label="",style="solid", color="burlywood", weight=9];
222 -> 108[label="",style="solid", color="burlywood", weight=3];
95[label="vx500",fontsize=16,color="green",shape="box"];96[label="vx400",fontsize=16,color="green",shape="box"];142[label="primMulNat vx410 vx510",fontsize=16,color="burlywood",shape="triangle"];223[label="vx410/Succ vx4100",fontsize=10,color="white",style="solid",shape="box"];142 -> 223[label="",style="solid", color="burlywood", weight=9];
223 -> 150[label="",style="solid", color="burlywood", weight=3];
224[label="vx410/Zero",fontsize=10,color="white",style="solid",shape="box"];142 -> 224[label="",style="solid", color="burlywood", weight=9];
224 -> 151[label="",style="solid", color="burlywood", weight=3];
141 -> 142[label="",style="dashed", color="red", weight=0];
141[label="primMulNat vx6 (Succ (Succ Zero))",fontsize=16,color="magenta"];141 -> 152[label="",style="dashed", color="magenta", weight=3];
141 -> 153[label="",style="dashed", color="magenta", weight=3];
143 -> 142[label="",style="dashed", color="red", weight=0];
143[label="primMulNat vx410 vx510",fontsize=16,color="magenta"];143 -> 154[label="",style="dashed", color="magenta", weight=3];
100[label="vx5000",fontsize=16,color="green",shape="box"];101[label="vx4000",fontsize=16,color="green",shape="box"];102[label="Pos (primMulNat (Succ vx4000) (Succ Zero))",fontsize=16,color="green",shape="box"];102 -> 113[label="",style="dashed", color="green", weight=3];
103[label="Neg (primMulNat (Succ vx5000) (Succ Zero))",fontsize=16,color="green",shape="box"];103 -> 114[label="",style="dashed", color="green", weight=3];
104[label="Pos (primMulNat Zero (Succ Zero))",fontsize=16,color="green",shape="box"];104 -> 115[label="",style="dashed", color="green", weight=3];
105[label="primMulNat (primPlusNat (Succ vx4000) (Succ vx5000)) (Succ Zero)",fontsize=16,color="black",shape="box"];105 -> 116[label="",style="solid", color="black", weight=3];
106[label="primMulNat (primPlusNat (Succ vx4000) Zero) (Succ Zero)",fontsize=16,color="black",shape="box"];106 -> 117[label="",style="solid", color="black", weight=3];
107[label="primMulNat (primPlusNat Zero (Succ vx5000)) (Succ Zero)",fontsize=16,color="black",shape="box"];107 -> 118[label="",style="solid", color="black", weight=3];
108[label="primMulNat (primPlusNat Zero Zero) (Succ Zero)",fontsize=16,color="black",shape="box"];108 -> 119[label="",style="solid", color="black", weight=3];
150[label="primMulNat (Succ vx4100) vx510",fontsize=16,color="burlywood",shape="box"];227[label="vx510/Succ vx5100",fontsize=10,color="white",style="solid",shape="box"];150 -> 227[label="",style="solid", color="burlywood", weight=9];
227 -> 163[label="",style="solid", color="burlywood", weight=3];
228[label="vx510/Zero",fontsize=10,color="white",style="solid",shape="box"];150 -> 228[label="",style="solid", color="burlywood", weight=9];
228 -> 164[label="",style="solid", color="burlywood", weight=3];
151[label="primMulNat Zero vx510",fontsize=16,color="burlywood",shape="box"];229[label="vx510/Succ vx5100",fontsize=10,color="white",style="solid",shape="box"];151 -> 229[label="",style="solid", color="burlywood", weight=9];
229 -> 165[label="",style="solid", color="burlywood", weight=3];
230[label="vx510/Zero",fontsize=10,color="white",style="solid",shape="box"];151 -> 230[label="",style="solid", color="burlywood", weight=9];
230 -> 166[label="",style="solid", color="burlywood", weight=3];
152[label="Succ (Succ Zero)",fontsize=16,color="green",shape="box"];153[label="vx6",fontsize=16,color="green",shape="box"];154[label="vx510",fontsize=16,color="green",shape="box"];113[label="primMulNat (Succ vx4000) (Succ Zero)",fontsize=16,color="black",shape="triangle"];113 -> 124[label="",style="solid", color="black", weight=3];
114 -> 113[label="",style="dashed", color="red", weight=0];
114[label="primMulNat (Succ vx5000) (Succ Zero)",fontsize=16,color="magenta"];114 -> 125[label="",style="dashed", color="magenta", weight=3];
115[label="primMulNat Zero (Succ Zero)",fontsize=16,color="black",shape="triangle"];115 -> 126[label="",style="solid", color="black", weight=3];
116 -> 113[label="",style="dashed", color="red", weight=0];
116[label="primMulNat (Succ (Succ (primPlusNat vx4000 vx5000))) (Succ Zero)",fontsize=16,color="magenta"];116 -> 127[label="",style="dashed", color="magenta", weight=3];
117 -> 113[label="",style="dashed", color="red", weight=0];
117[label="primMulNat (Succ vx4000) (Succ Zero)",fontsize=16,color="magenta"];118 -> 113[label="",style="dashed", color="red", weight=0];
118[label="primMulNat (Succ vx5000) (Succ Zero)",fontsize=16,color="magenta"];118 -> 128[label="",style="dashed", color="magenta", weight=3];
119 -> 115[label="",style="dashed", color="red", weight=0];
119[label="primMulNat Zero (Succ Zero)",fontsize=16,color="magenta"];163[label="primMulNat (Succ vx4100) (Succ vx5100)",fontsize=16,color="black",shape="box"];163 -> 173[label="",style="solid", color="black", weight=3];
164[label="primMulNat (Succ vx4100) Zero",fontsize=16,color="black",shape="box"];164 -> 174[label="",style="solid", color="black", weight=3];
165[label="primMulNat Zero (Succ vx5100)",fontsize=16,color="black",shape="box"];165 -> 175[label="",style="solid", color="black", weight=3];
166[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];166 -> 176[label="",style="solid", color="black", weight=3];
124[label="primPlusNat (primMulNat vx4000 (Succ Zero)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];236[label="vx4000/Succ vx40000",fontsize=10,color="white",style="solid",shape="box"];124 -> 236[label="",style="solid", color="burlywood", weight=9];
236 -> 132[label="",style="solid", color="burlywood", weight=3];
237[label="vx4000/Zero",fontsize=10,color="white",style="solid",shape="box"];124 -> 237[label="",style="solid", color="burlywood", weight=9];
237 -> 133[label="",style="solid", color="burlywood", weight=3];
125[label="vx5000",fontsize=16,color="green",shape="box"];126[label="Zero",fontsize=16,color="green",shape="box"];127[label="Succ (primPlusNat vx4000 vx5000)",fontsize=16,color="green",shape="box"];127 -> 134[label="",style="dashed", color="green", weight=3];
128[label="vx5000",fontsize=16,color="green",shape="box"];173 -> 134[label="",style="dashed", color="red", weight=0];
173[label="primPlusNat (primMulNat vx4100 (Succ vx5100)) (Succ vx5100)",fontsize=16,color="magenta"];173 -> 180[label="",style="dashed", color="magenta", weight=3];
173 -> 181[label="",style="dashed", color="magenta", weight=3];
174[label="Zero",fontsize=16,color="green",shape="box"];175[label="Zero",fontsize=16,color="green",shape="box"];176[label="Zero",fontsize=16,color="green",shape="box"];132[label="primPlusNat (primMulNat (Succ vx40000) (Succ Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];132 -> 137[label="",style="solid", color="black", weight=3];
133[label="primPlusNat (primMulNat Zero (Succ Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];133 -> 138[label="",style="solid", color="black", weight=3];
134[label="primPlusNat vx4000 vx5000",fontsize=16,color="burlywood",shape="triangle"];239[label="vx4000/Succ vx40000",fontsize=10,color="white",style="solid",shape="box"];134 -> 239[label="",style="solid", color="burlywood", weight=9];
239 -> 139[label="",style="solid", color="burlywood", weight=3];
240[label="vx4000/Zero",fontsize=10,color="white",style="solid",shape="box"];134 -> 240[label="",style="solid", color="burlywood", weight=9];
240 -> 140[label="",style="solid", color="burlywood", weight=3];
180[label="Succ vx5100",fontsize=16,color="green",shape="box"];181 -> 142[label="",style="dashed", color="red", weight=0];
181[label="primMulNat vx4100 (Succ vx5100)",fontsize=16,color="magenta"];181 -> 184[label="",style="dashed", color="magenta", weight=3];
181 -> 185[label="",style="dashed", color="magenta", weight=3];
137 -> 134[label="",style="dashed", color="red", weight=0];
137[label="primPlusNat (primPlusNat (primMulNat vx40000 (Succ Zero)) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];137 -> 155[label="",style="dashed", color="magenta", weight=3];
137 -> 156[label="",style="dashed", color="magenta", weight=3];
138 -> 134[label="",style="dashed", color="red", weight=0];
138[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];138 -> 157[label="",style="dashed", color="magenta", weight=3];
138 -> 158[label="",style="dashed", color="magenta", weight=3];
139[label="primPlusNat (Succ vx40000) vx5000",fontsize=16,color="burlywood",shape="box"];244[label="vx5000/Succ vx50000",fontsize=10,color="white",style="solid",shape="box"];139 -> 244[label="",style="solid", color="burlywood", weight=9];
244 -> 159[label="",style="solid", color="burlywood", weight=3];
245[label="vx5000/Zero",fontsize=10,color="white",style="solid",shape="box"];139 -> 245[label="",style="solid", color="burlywood", weight=9];
245 -> 160[label="",style="solid", color="burlywood", weight=3];
140[label="primPlusNat Zero vx5000",fontsize=16,color="burlywood",shape="box"];246[label="vx5000/Succ vx50000",fontsize=10,color="white",style="solid",shape="box"];140 -> 246[label="",style="solid", color="burlywood", weight=9];
246 -> 161[label="",style="solid", color="burlywood", weight=3];
247[label="vx5000/Zero",fontsize=10,color="white",style="solid",shape="box"];140 -> 247[label="",style="solid", color="burlywood", weight=9];
247 -> 162[label="",style="solid", color="burlywood", weight=3];
184[label="Succ vx5100",fontsize=16,color="green",shape="box"];185[label="vx4100",fontsize=16,color="green",shape="box"];155[label="Succ Zero",fontsize=16,color="green",shape="box"];156 -> 134[label="",style="dashed", color="red", weight=0];
156[label="primPlusNat (primMulNat vx40000 (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];156 -> 167[label="",style="dashed", color="magenta", weight=3];
156 -> 168[label="",style="dashed", color="magenta", weight=3];
157[label="Succ Zero",fontsize=16,color="green",shape="box"];158[label="Zero",fontsize=16,color="green",shape="box"];159[label="primPlusNat (Succ vx40000) (Succ vx50000)",fontsize=16,color="black",shape="box"];159 -> 169[label="",style="solid", color="black", weight=3];
160[label="primPlusNat (Succ vx40000) Zero",fontsize=16,color="black",shape="box"];160 -> 170[label="",style="solid", color="black", weight=3];
161[label="primPlusNat Zero (Succ vx50000)",fontsize=16,color="black",shape="box"];161 -> 171[label="",style="solid", color="black", weight=3];
162[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];162 -> 172[label="",style="solid", color="black", weight=3];
167[label="Succ Zero",fontsize=16,color="green",shape="box"];168 -> 142[label="",style="dashed", color="red", weight=0];
168[label="primMulNat vx40000 (Succ Zero)",fontsize=16,color="magenta"];168 -> 177[label="",style="dashed", color="magenta", weight=3];
168 -> 178[label="",style="dashed", color="magenta", weight=3];
169[label="Succ (Succ (primPlusNat vx40000 vx50000))",fontsize=16,color="green",shape="box"];169 -> 179[label="",style="dashed", color="green", weight=3];
170[label="Succ vx40000",fontsize=16,color="green",shape="box"];171[label="Succ vx50000",fontsize=16,color="green",shape="box"];172[label="Zero",fontsize=16,color="green",shape="box"];177[label="Succ Zero",fontsize=16,color="green",shape="box"];178[label="vx40000",fontsize=16,color="green",shape="box"];179 -> 134[label="",style="dashed", color="red", weight=0];
179[label="primPlusNat vx40000 vx50000",fontsize=16,color="magenta"];179 -> 182[label="",style="dashed", color="magenta", weight=3];
179 -> 183[label="",style="dashed", color="magenta", weight=3];
182[label="vx50000",fontsize=16,color="green",shape="box"];183[label="vx40000",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx40000), Succ(vx50000)) → new_primPlusNat(vx40000, vx50000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vx40000), Succ(vx50000)) → new_primPlusNat(vx40000, vx50000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vx4100), Succ(vx5100)) → new_primMulNat(vx4100, Succ(vx5100))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(vx4100), Succ(vx5100)) → new_primMulNat(vx4100, Succ(vx5100))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primMulInt(Succ(vx4000), Succ(vx5000)) → new_primMulInt(vx4000, vx5000)

From the DPs we obtained the following set of size-change graphs:

new_primMulInt(Succ(vx4000), Succ(vx5000)) → new_primMulInt(vx4000, vx5000)
The graph contains the following edges 1 > 1, 2 > 2